KILLED



    


Runtime Complexity (innermost) proof of /tmp/tmpTrp59_/bfs.raml.xml









The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

0 CpxRelTRS


↳1 DecreasingLoopProof (⇔, 1384 ms)


↳2 BOUNDS(n^1, INF)


↳3 RenamingProof (⇔, 0 ms)


↳4 CpxRelTRS


    ↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)


    ↳6 typed CpxTrs


    ↳7 OrderProof (LOWER BOUND(ID), 1 ms)


    ↳8 typed CpxTrs









(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#equal(@x, @y) → #eq(@x, @y)

appendreverse(@toreverse, @sofar) → appendreverse#1(@toreverse, @sofar)

appendreverse#1(::(@a, @as), @sofar) → appendreverse(@as, ::(@a, @sofar))

appendreverse#1(nil, @sofar) → @sofar

bfs(@queue, @futurequeue, @x) → bfs#1(@queue, @futurequeue, @x)

bfs#1(::(@t, @ts), @futurequeue, @x) → bfs#3(@t, @futurequeue, @ts, @x)

bfs#1(nil, @futurequeue, @x) → bfs#2(@futurequeue, @x)

bfs#2(::(@t, @ts), @x) → bfs(reverse(::(@t, @ts)), nil, @x)

bfs#2(nil, @x) → leaf

bfs#3(leaf, @futurequeue, @ts, @x) → bfs(@ts, @futurequeue, @x)

bfs#3(node(@y, @t1, @t2), @futurequeue, @ts, @x) → bfs#4(#equal(@x, @y), @futurequeue, @t1, @t2, @ts, @x, @y)

bfs#4(#false, @futurequeue, @t1, @t2, @ts, @x, @y) → bfs(@ts, ::(@t2, ::(@t1, @futurequeue)), @x)

bfs#4(#true, @futurequeue, @t1, @t2, @ts, @x, @y) → node(@y, @t1, @t2)

bfs2(@t, @x) → bfs2#1(dobfs(@t, @x), @x)

bfs2#1(@t', @x) → dobfs(@t', @x)

dfs(@queue, @x) → dfs#1(@queue, @x)

dfs#1(::(@t, @ts), @x) → dfs#2(@t, @t, @ts, @x)

dfs#1(nil, @x) → leaf

dfs#2(leaf, @t, @ts, @x) → dfs(@ts, @x)

dfs#2(node(@a, @t1, @t2), @t, @ts, @x) → dfs#3(#equal(@a, @x), @t, @t1, @t2, @ts, @x)

dfs#3(#false, @t, @t1, @t2, @ts, @x) → dfs(::(@t1, ::(@t2, @ts)), @x)

dfs#3(#true, @t, @t1, @t2, @ts, @x) → @t

dobfs(@t, @x) → bfs(::(@t, nil), nil, @x)

dodfs(@t, @x) → dfs(::(@t, nil), @x)

reverse(@xs) → appendreverse(@xs, nil)

The (relative) TRS S consists of the following rules:

#and(#false, #false) → #false

#and(#false, #true) → #false

#and(#true, #false) → #false

#and(#true, #true) → #true

#eq(#0, #0) → #true

#eq(#0, #neg(@y)) → #false

#eq(#0, #pos(@y)) → #false

#eq(#0, #s(@y)) → #false

#eq(#neg(@x), #0) → #false

#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)

#eq(#neg(@x), #pos(@y)) → #false

#eq(#pos(@x), #0) → #false

#eq(#pos(@x), #neg(@y)) → #false

#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)

#eq(#s(@x), #0) → #false

#eq(#s(@x), #s(@y)) → #eq(@x, @y)

#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))

#eq(::(@x_1, @x_2), leaf) → #false

#eq(::(@x_1, @x_2), nil) → #false

#eq(::(@x_1, @x_2), node(@y_1, @y_2, @y_3)) → #false

#eq(leaf, ::(@y_1, @y_2)) → #false

#eq(leaf, leaf) → #true

#eq(leaf, nil) → #false

#eq(leaf, node(@y_1, @y_2, @y_3)) → #false

#eq(nil, ::(@y_1, @y_2)) → #false

#eq(nil, leaf) → #false

#eq(nil, nil) → #true

#eq(nil, node(@y_1, @y_2, @y_3)) → #false

#eq(node(@x_1, @x_2, @x_3), ::(@y_1, @y_2)) → #false

#eq(node(@x_1, @x_2, @x_3), leaf) → #false

#eq(node(@x_1, @x_2, @x_3), nil) → #false

#eq(node(@x_1, @x_2, @x_3), node(@y_1, @y_2, @y_3)) → #and(#eq(@x_1, @y_1), #and(#eq(@x_2, @y_2), #eq(@x_3, @y_3)))

Rewrite Strategy: INNERMOST




(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
appendreverse(::(@a4229_5, @as4230_5), @sofar) →+ appendreverse(@as4230_5, ::(@a4229_5, @sofar))
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [@as4230_5 / ::(@a4229_5, @as4230_5)].
The result substitution is [@sofar / ::(@a4229_5, @sofar)].





(2) BOUNDS(n^1, INF)




(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.




(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#equal(@x, @y) → #eq(@x, @y)

appendreverse(@toreverse, @sofar) → appendreverse#1(@toreverse, @sofar)

appendreverse#1(::(@a, @as), @sofar) → appendreverse(@as, ::(@a, @sofar))

appendreverse#1(nil, @sofar) → @sofar

bfs(@queue, @futurequeue, @x) → bfs#1(@queue, @futurequeue, @x)

bfs#1(::(@t, @ts), @futurequeue, @x) → bfs#3(@t, @futurequeue, @ts, @x)

bfs#1(nil, @futurequeue, @x) → bfs#2(@futurequeue, @x)

bfs#2(::(@t, @ts), @x) → bfs(reverse(::(@t, @ts)), nil, @x)

bfs#2(nil, @x) → leaf

bfs#3(leaf, @futurequeue, @ts, @x) → bfs(@ts, @futurequeue, @x)

bfs#3(node(@y, @t1, @t2), @futurequeue, @ts, @x) → bfs#4(#equal(@x, @y), @futurequeue, @t1, @t2, @ts, @x, @y)

bfs#4(#false, @futurequeue, @t1, @t2, @ts, @x, @y) → bfs(@ts, ::(@t2, ::(@t1, @futurequeue)), @x)

bfs#4(#true, @futurequeue, @t1, @t2, @ts, @x, @y) → node(@y, @t1, @t2)

bfs2(@t, @x) → bfs2#1(dobfs(@t, @x), @x)

bfs2#1(@t', @x) → dobfs(@t', @x)

dfs(@queue, @x) → dfs#1(@queue, @x)

dfs#1(::(@t, @ts), @x) → dfs#2(@t, @t, @ts, @x)

dfs#1(nil, @x) → leaf

dfs#2(leaf, @t, @ts, @x) → dfs(@ts, @x)

dfs#2(node(@a, @t1, @t2), @t, @ts, @x) → dfs#3(#equal(@a, @x), @t, @t1, @t2, @ts, @x)

dfs#3(#false, @t, @t1, @t2, @ts, @x) → dfs(::(@t1, ::(@t2, @ts)), @x)

dfs#3(#true, @t, @t1, @t2, @ts, @x) → @t

dobfs(@t, @x) → bfs(::(@t, nil), nil, @x)

dodfs(@t, @x) → dfs(::(@t, nil), @x)

reverse(@xs) → appendreverse(@xs, nil)

The (relative) TRS S consists of the following rules:

#and(#false, #false) → #false

#and(#false, #true) → #false

#and(#true, #false) → #false

#and(#true, #true) → #true

#eq(#0, #0) → #true

#eq(#0, #neg(@y)) → #false

#eq(#0, #pos(@y)) → #false

#eq(#0, #s(@y)) → #false

#eq(#neg(@x), #0) → #false

#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)

#eq(#neg(@x), #pos(@y)) → #false

#eq(#pos(@x), #0) → #false

#eq(#pos(@x), #neg(@y)) → #false

#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)

#eq(#s(@x), #0) → #false

#eq(#s(@x), #s(@y)) → #eq(@x, @y)

#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))

#eq(::(@x_1, @x_2), leaf) → #false

#eq(::(@x_1, @x_2), nil) → #false

#eq(::(@x_1, @x_2), node(@y_1, @y_2, @y_3)) → #false

#eq(leaf, ::(@y_1, @y_2)) → #false

#eq(leaf, leaf) → #true

#eq(leaf, nil) → #false

#eq(leaf, node(@y_1, @y_2, @y_3)) → #false

#eq(nil, ::(@y_1, @y_2)) → #false

#eq(nil, leaf) → #false

#eq(nil, nil) → #true

#eq(nil, node(@y_1, @y_2, @y_3)) → #false

#eq(node(@x_1, @x_2, @x_3), ::(@y_1, @y_2)) → #false

#eq(node(@x_1, @x_2, @x_3), leaf) → #false

#eq(node(@x_1, @x_2, @x_3), nil) → #false

#eq(node(@x_1, @x_2, @x_3), node(@y_1, @y_2, @y_3)) → #and(#eq(@x_1, @y_1), #and(#eq(@x_2, @y_2), #eq(@x_3, @y_3)))

Rewrite Strategy: INNERMOST




(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.




(6) Obligation:
Innermost TRS:
Rules:
#equal(@x, @y) → #eq(@x, @y)
appendreverse(@toreverse, @sofar) → appendreverse#1(@toreverse, @sofar)
appendreverse#1(::(@a, @as), @sofar) → appendreverse(@as, ::(@a, @sofar))
appendreverse#1(nil, @sofar) → @sofar
bfs(@queue, @futurequeue, @x) → bfs#1(@queue, @futurequeue, @x)
bfs#1(::(@t, @ts), @futurequeue, @x) → bfs#3(@t, @futurequeue, @ts, @x)
bfs#1(nil, @futurequeue, @x) → bfs#2(@futurequeue, @x)
bfs#2(::(@t, @ts), @x) → bfs(reverse(::(@t, @ts)), nil, @x)
bfs#2(nil, @x) → leaf
bfs#3(leaf, @futurequeue, @ts, @x) → bfs(@ts, @futurequeue, @x)
bfs#3(node(@y, @t1, @t2), @futurequeue, @ts, @x) → bfs#4(#equal(@x, @y), @futurequeue, @t1, @t2, @ts, @x, @y)
bfs#4(#false, @futurequeue, @t1, @t2, @ts, @x, @y) → bfs(@ts, ::(@t2, ::(@t1, @futurequeue)), @x)
bfs#4(#true, @futurequeue, @t1, @t2, @ts, @x, @y) → node(@y, @t1, @t2)
bfs2(@t, @x) → bfs2#1(dobfs(@t, @x), @x)
bfs2#1(@t', @x) → dobfs(@t', @x)
dfs(@queue, @x) → dfs#1(@queue, @x)
dfs#1(::(@t, @ts), @x) → dfs#2(@t, @t, @ts, @x)
dfs#1(nil, @x) → leaf
dfs#2(leaf, @t, @ts, @x) → dfs(@ts, @x)
dfs#2(node(@a, @t1, @t2), @t, @ts, @x) → dfs#3(#equal(@a, @x), @t, @t1, @t2, @ts, @x)
dfs#3(#false, @t, @t1, @t2, @ts, @x) → dfs(::(@t1, ::(@t2, @ts)), @x)
dfs#3(#true, @t, @t1, @t2, @ts, @x) → @t
dobfs(@t, @x) → bfs(::(@t, nil), nil, @x)
dodfs(@t, @x) → dfs(::(@t, nil), @x)
reverse(@xs) → appendreverse(@xs, nil)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), leaf) → #false
#eq(::(@x_1, @x_2), nil) → #false
#eq(::(@x_1, @x_2), node(@y_1, @y_2, @y_3)) → #false
#eq(leaf, ::(@y_1, @y_2)) → #false
#eq(leaf, leaf) → #true
#eq(leaf, nil) → #false
#eq(leaf, node(@y_1, @y_2, @y_3)) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, leaf) → #false
#eq(nil, nil) → #true
#eq(nil, node(@y_1, @y_2, @y_3)) → #false
#eq(node(@x_1, @x_2, @x_3), ::(@y_1, @y_2)) → #false
#eq(node(@x_1, @x_2, @x_3), leaf) → #false
#eq(node(@x_1, @x_2, @x_3), nil) → #false
#eq(node(@x_1, @x_2, @x_3), node(@y_1, @y_2, @y_3)) → #and(#eq(@x_1, @y_1), #and(#eq(@x_2, @y_2), #eq(@x_3, @y_3)))

Types:
#equal :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → #false:#true
appendreverse :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
appendreverse#1 :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
:: :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
nil :: :::nil:leaf:node:#0:#neg:#pos:#s
bfs :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
bfs#1 :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
bfs#3 :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
bfs#2 :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
reverse :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
leaf :: :::nil:leaf:node:#0:#neg:#pos:#s
node :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
bfs#4 :: #false:#true → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
bfs2 :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
bfs2#1 :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
dobfs :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
dfs :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
dfs#1 :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
dfs#2 :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
dfs#3 :: #false:#true → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
dodfs :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
#and :: #false:#true → #false:#true → #false:#true
#0 :: :::nil:leaf:node:#0:#neg:#pos:#s
#neg :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
#pos :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
#s :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
hole_#false:#true1_5 :: #false:#true
hole_:::nil:leaf:node:#0:#neg:#pos:#s2_5 :: :::nil:leaf:node:#0:#neg:#pos:#s
gen_:::nil:leaf:node:#0:#neg:#pos:#s3_5 :: Nat → :::nil:leaf:node:#0:#neg:#pos:#s




(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
#eq, appendreverse, appendreverse#1, bfs, bfs#1, bfs#2, dfs, dfs#1
They will be analysed ascendingly in the following order:
appendreverse = appendreverse#1
bfs = bfs#1
bfs = bfs#2
bfs#1 = bfs#2
dfs = dfs#1




(8) Obligation:
Innermost TRS:
Rules:
#equal(@x, @y) → #eq(@x, @y)
appendreverse(@toreverse, @sofar) → appendreverse#1(@toreverse, @sofar)
appendreverse#1(::(@a, @as), @sofar) → appendreverse(@as, ::(@a, @sofar))
appendreverse#1(nil, @sofar) → @sofar
bfs(@queue, @futurequeue, @x) → bfs#1(@queue, @futurequeue, @x)
bfs#1(::(@t, @ts), @futurequeue, @x) → bfs#3(@t, @futurequeue, @ts, @x)
bfs#1(nil, @futurequeue, @x) → bfs#2(@futurequeue, @x)
bfs#2(::(@t, @ts), @x) → bfs(reverse(::(@t, @ts)), nil, @x)
bfs#2(nil, @x) → leaf
bfs#3(leaf, @futurequeue, @ts, @x) → bfs(@ts, @futurequeue, @x)
bfs#3(node(@y, @t1, @t2), @futurequeue, @ts, @x) → bfs#4(#equal(@x, @y), @futurequeue, @t1, @t2, @ts, @x, @y)
bfs#4(#false, @futurequeue, @t1, @t2, @ts, @x, @y) → bfs(@ts, ::(@t2, ::(@t1, @futurequeue)), @x)
bfs#4(#true, @futurequeue, @t1, @t2, @ts, @x, @y) → node(@y, @t1, @t2)
bfs2(@t, @x) → bfs2#1(dobfs(@t, @x), @x)
bfs2#1(@t', @x) → dobfs(@t', @x)
dfs(@queue, @x) → dfs#1(@queue, @x)
dfs#1(::(@t, @ts), @x) → dfs#2(@t, @t, @ts, @x)
dfs#1(nil, @x) → leaf
dfs#2(leaf, @t, @ts, @x) → dfs(@ts, @x)
dfs#2(node(@a, @t1, @t2), @t, @ts, @x) → dfs#3(#equal(@a, @x), @t, @t1, @t2, @ts, @x)
dfs#3(#false, @t, @t1, @t2, @ts, @x) → dfs(::(@t1, ::(@t2, @ts)), @x)
dfs#3(#true, @t, @t1, @t2, @ts, @x) → @t
dobfs(@t, @x) → bfs(::(@t, nil), nil, @x)
dodfs(@t, @x) → dfs(::(@t, nil), @x)
reverse(@xs) → appendreverse(@xs, nil)
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), leaf) → #false
#eq(::(@x_1, @x_2), nil) → #false
#eq(::(@x_1, @x_2), node(@y_1, @y_2, @y_3)) → #false
#eq(leaf, ::(@y_1, @y_2)) → #false
#eq(leaf, leaf) → #true
#eq(leaf, nil) → #false
#eq(leaf, node(@y_1, @y_2, @y_3)) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, leaf) → #false
#eq(nil, nil) → #true
#eq(nil, node(@y_1, @y_2, @y_3)) → #false
#eq(node(@x_1, @x_2, @x_3), ::(@y_1, @y_2)) → #false
#eq(node(@x_1, @x_2, @x_3), leaf) → #false
#eq(node(@x_1, @x_2, @x_3), nil) → #false
#eq(node(@x_1, @x_2, @x_3), node(@y_1, @y_2, @y_3)) → #and(#eq(@x_1, @y_1), #and(#eq(@x_2, @y_2), #eq(@x_3, @y_3)))

Types:
#equal :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → #false:#true
appendreverse :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
appendreverse#1 :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
:: :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
nil :: :::nil:leaf:node:#0:#neg:#pos:#s
bfs :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
bfs#1 :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
bfs#3 :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
bfs#2 :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
reverse :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
leaf :: :::nil:leaf:node:#0:#neg:#pos:#s
node :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
bfs#4 :: #false:#true → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
bfs2 :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
bfs2#1 :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
dobfs :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
dfs :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
dfs#1 :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
dfs#2 :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
dfs#3 :: #false:#true → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
dodfs :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
#and :: #false:#true → #false:#true → #false:#true
#0 :: :::nil:leaf:node:#0:#neg:#pos:#s
#neg :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
#pos :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
#s :: :::nil:leaf:node:#0:#neg:#pos:#s → :::nil:leaf:node:#0:#neg:#pos:#s
hole_#false:#true1_5 :: #false:#true
hole_:::nil:leaf:node:#0:#neg:#pos:#s2_5 :: :::nil:leaf:node:#0:#neg:#pos:#s
gen_:::nil:leaf:node:#0:#neg:#pos:#s3_5 :: Nat → :::nil:leaf:node:#0:#neg:#pos:#s
Generator Equations:
gen_:::nil:leaf:node:#0:#neg:#pos:#s3_5(0) ⇔ nil
gen_:::nil:leaf:node:#0:#neg:#pos:#s3_5(+(x, 1)) ⇔ ::(nil, gen_:::nil:leaf:node:#0:#neg:#pos:#s3_5(x))
The following defined symbols remain to be analysed:
#eq, appendreverse, appendreverse#1, bfs, bfs#1, bfs#2, dfs, dfs#1
They will be analysed ascendingly in the following order:
appendreverse = appendreverse#1
bfs = bfs#1
bfs = bfs#2
bfs#1 = bfs#2
dfs = dfs#1